FDL - Nuprl Lemma : es-rcv-from

Nuprl Lemma : es-rcv-from_wf

es:event_system{i:l}, e:es-E(es), l:IdLnk, L:(es-E(es) List).
es-rcv-from(es; e; l; L)

prop{i:l}

Definitions x:A. B(x), t T, prop{i:l}, es-rcv-from(es; e; l; L), A c B, P Q, P Q, P Q, P Q

Lemmas es-E wf, iff wf, l member wf, assert wf, es-isrcv wf, IdLnk wf, es-lnk wf, es-sender wf, l before wf, es-locl wf, event system wf

Definitions	x:A. B(x), t T, prop{i:l}, es-rcv-from(es; e; l; L), A c B, P Q, P Q, P Q, P Q
Lemmas	es-E wf, iff wf, l member wf, assert wf, es-isrcv wf, IdLnk wf, es-lnk wf, es-sender wf, l before wf, es-locl wf, event system wf